Nuprl Lemma : w-atom-constraint_wf
11,40
postcript
pdf
w
:world{i:l}. w-atom-constraint{i:l}(
w
)
{i'}
latex
Definitions
w-atom-constraint(
w
)
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
world
wf
,
true
wf
origin
w:world{i:l}. w-atom-constraint{i:l}(w) 
{i'} w:world{i:l}. w-atom-constraint{i:l}(w) {i'} Tx:A. B(x)